Definitions | i j < k, t T, Y, P & Q, {i..j }, ||as||, ( x,y L. P(x;y)), P  Q, x:A. B(x), AbsInterface(A), , Top, S T, e  X, {T}, suptype(S; T),  x. t(x), P Q, P   Q, P  Q,  x,y. t(x;y), E(X), A, X Y = 0, R1   R2, A c B, x f y, {I}, R|P, R1 R2, False, x:A. B(x), Q-R-glued(es; Ib_valtype; f; Ia; Qa; Ib; Rb), T, True, A B, (x l), ( x L.P(x)), Dec(P), x(s), x(s1,s2), x L. P(x),  |